move_swap_left: Composing a transposition with (a b)
This lemma proves that when you multiply any transposition σ by (a b), one of two things happens: either they cancel (if σ = (a b)), or the result can be rewritten as (a z) · τ where τ is a transposition that fixes a. The key insight is a case analysis: depending on whether σ shares elements with {a, b}, we use different commutation rules (swap_mul_swap_share_left, swap_mul_swap_share_right, or swap_mul_swap_comm_of_disjoint) to "move the a to the left". This is crucial for algorithms that normalize permutations by repeatedly conjugating transpositions.
Interactive Lean 4 proof — click a line to see its strategy and explanation inline
Strategy: State the lemma — composing a transposition σ with (a b) either cancels or factors as (a z) · τ with τ fixing a.
Explanation: Given a transposition σ and a distinct pair a ≠ b, we claim that σ · (a b) either equals the identity (cancellation case), or can be written as (a z) · τ where z ≠ a, τ is a transposition, and τ(a) = a. This is the key technical lemma for "moving a to the left" in permutation algorithms, and it's proved by exhaustive case analysis on how σ overlaps with {a, b}.
Strategy: Destruct the IsSwap hypothesis to obtain concrete elements x, y with σ = swap x y.
Explanation: The hypothesis hσ : σ.IsSwap unfolds to ∃ x y, x ≠ y ∧ σ = swap x y. We use rcases to extract witnesses x, y, the proof hxy : x ≠ y, and substitute σ := swap x y via rfl. From now on, the goal is about swap x y * swap a b, and we proceed by case analysis on how {x, y} overlaps with {a, b}.
Strategy: First case split — test whether σ equals (a b).
Explanation: We use by_cases to split on whether swap x y = swap a b (which includes swap b a by commutativity of swap). If true, we're in the cancellation case and will take the left disjunct (σ * swap a b = 1). Otherwise, we proceed to the right disjunct and further case-split on how {x, y} overlaps {a, b}.
Strategy: Cancellation case — if σ = (a b), then σ · (a b) = 1.
Explanation: Given h : swap x y = swap a b, we rewrite the goal to swap a b * swap a b, which equals 1 by Equiv.swap_mul_self (a transposition is its own inverse). We choose the left disjunct, proving σ * swap a b = 1. This closes the cancellation branch.
Strategy: Non-cancellation case — choose the right disjunct and begin case analysis on overlap with a.
Explanation: Since swap x y ≠ swap a b, we must prove the right disjunct: ∃ z ≠ a, ∃ τ fixing a, σ * swap a b = swap a z * τ. We use an if statement to check whether σ involves a (i.e., x = a or y = a). This is the first of three sub-cases. If true, we'll use swap_mul_swap_share_left to rewrite the product.
Strategy: Normalize σ to the form (a z) for some z ≠ a.
Explanation: We prove ∃ z ≠ a, swap x y = swap a z. If x = a, take z := y (using hxy.symm : y ≠ x = a); if y = a, take z := x and use Equiv.swap_comm to rewrite swap x y = swap y x = swap a x. This gives us σ = swap a z for some z ≠ a, which is the form we need for the next step.
Strategy: Substitute σ = swap a z and prove z ≠ b.
Explanation: We rewrite the goal using heq, so now we work with swap a z * swap a b. We prove z ≠ b by contradiction: if z = b, then by heq, swap x y = swap a b, contradicting h. This inequality is needed as a hypothesis for swap_mul_swap_share_left.
Strategy: Provide witnesses for the existential — take z := b and τ := swap b z.
Explanation: We use refine to provide the witnesses: z' := b (with b ≠ a by hab.symm), and τ := swap b z. We package the IsSwap proof for τ as ⟨b, z, by aesop, rfl⟩, where aesop solves b ≠ z from hzb. This leaves two sub-goals: (1) τ a = a, and (2) swap a z * swap a b = swap a b * τ.
Strategy: Prove τ a = a, i.e., swap b z fixes a.
Explanation: We must show (swap b z) a = a. Unfolding swap_apply_def with simp, this reduces to: if a = b then z else if a = z then b else a. Since a ≠ b (by hab) and a ≠ z (by hza), the result is a. aesop closes this arithmetic goal using the hypotheses.
Strategy: Prove the factorization swap a z * swap a b = swap a b * swap b z using the share_left lemma.
Explanation: The lemma swap_mul_swap_share_left states: for z ≠ b and z ≠ a, swap a z * swap a b = swap a b * swap b z. This is exactly what we need. Applying it with hzb and hza closes the goal. This completes the "σ involves a" case.
Strategy: Second sub-case — σ involves b but not a.
Explanation: Having ruled out the "σ involves a" case, we now test whether σ involves b. Combined with the negation of ha (pushed into scope by the else), we know x ≠ a and y ≠ a. If x = b or y = b, we'll normalize σ to swap b z and use swap_mul_swap_share_right.
Strategy: Normalize σ to the form (b z) for some z ≠ b.
Explanation: Analogous to the "σ involves a" case, we prove ∃ z ≠ b, swap x y = swap b z. If x = b, take z := y; if y = b, take z := x and use commutativity. This gives σ = swap b z.
Strategy: Substitute σ = swap b z and prove z ≠ a.
Explanation: Rewrite using heq, so now we work with swap b z * swap a b. We prove z ≠ a by contradiction: if z = a, then either x = b and y = a, or x = a and y = b. But the negation of ha tells us x ≠ a and y ≠ a, contradiction. The grind tactic closes both cases automatically.
Strategy: Provide witnesses — take z' := z and τ := swap z b.
Explanation: We instantiate the existential with z (which satisfies z ≠ a by hza) and τ := swap z b (with IsSwap proof ⟨z, b, hzb, rfl⟩). This leaves two sub-goals: (1) τ a = a, and (2) swap b z * swap a b = swap a z * swap z b.
Strategy: Prove τ a = a, i.e., swap z b fixes a.
Explanation: We show (swap z b) a = a. Unfolding swap_apply_def, this reduces to: if a = z then b else if a = b then z else a. Since a ≠ z (hza) and a ≠ b (hab), the result is a. aesop closes this.
Strategy: Prove the factorization swap b z * swap a b = swap a z * swap z b using the share_right lemma.
Explanation: The lemma swap_mul_swap_share_right states: for z ≠ a, z ≠ b, and a ≠ b, swap b z * swap a b = swap a z * swap z b. Applying it with hza, hzb, and hab closes the goal. This completes the "σ involves b but not a" case.
Strategy: Third sub-case — σ is disjoint from {a, b}.
Explanation: Having ruled out "σ involves a" and "σ involves b", we're in the else branch where neither x nor y equals a or b. We use push_neg to convert ¬(x = a ∨ y = a) and ¬(x = b ∨ y = b) into x ≠ a ∧ y ≠ a and x ≠ b ∧ y ≠ b, respectively. This means {x, y} is disjoint from {a, b}, so the transpositions commute.
Strategy: Prove the sets {a, b} and {x, y} are disjoint.
Explanation: We must show Disjoint ({a, b} : Set α) {x, y}. Using Set.disjoint_insert_left and Set.disjoint_singleton_left, this unfolds to: a ∉ {x, y} ∧ b ∉ {x, y}. From ha and hb (after push_neg), we have x ≠ a, y ≠ a, x ≠ b, y ≠ b, which imply these non-membership conditions. aesop closes this automatically.
Strategy: Provide witnesses — take z := b and τ := swap x y.
Explanation: We instantiate the existential with z' := b (satisfying b ≠ a by hab.symm) and τ := swap x y (with IsSwap proof ⟨x, y, hxy, rfl⟩). This leaves two sub-goals: (1) τ a = a, and (2) swap x y * swap a b = swap a b * swap x y (commutativity).
Strategy: Prove τ a = a, i.e., swap x y fixes a.
Explanation: We show (swap x y) a = a. Since a ≠ x and a ≠ y (from ha after push_neg), unfolding swap_apply_def gives a. aesop closes this.
Strategy: Prove the commutativity swap x y * swap a b = swap a b * swap x y using the disjoint lemma.
Explanation: The lemma swap_mul_swap_comm_of_disjoint states: if {a, b} is disjoint from {x, y}, then swap a b and swap x y commute. Applying it with hdisj closes the goal. This completes the disjoint case and the entire proof. □
💡 Tip: Click on any line above to see its strategy and explanation inline. Click again to hide it.
The proof follows an exhaustive case analysis on the overlap between σ = swap x y and {a, b}:
swap a z * swap a b = swap a b * swap b z
swap b z * swap a b = swap a z * swap z b
swap x y * swap a b = swap a b * swap x y
Key insight: In all non-cancellation cases, the product can be rewritten as (a z) · τ where τ fixes a. This is the algebraic foundation for algorithms that normalize permutations by "moving a element to the left" repeatedly. The proof is constructive: we explicitly provide z and τ in each case, and verify the factorization using the three auxiliary commutation lemmas.
For z ≠ b and z ≠ a, proves swap a z * swap a b = swap a b * swap b z.
Used when σ involves the left element a: we rewrite the product to move (a ·) to the front, producing (a b) · (b z) which fixes a.
This is the core algebraic transformation for the "σ involves a" case.
For z ≠ a, z ≠ b, and a ≠ b, proves swap b z * swap a b = swap a z * swap z b.
Used when σ involves the right element b but not a: we rewrite the product to factor out (a z) on the left,
with the remainder (z b) fixing a. This handles the "σ involves b" case.
When {a, b} is disjoint from {c, d}, proves swap a b * swap c d = swap c d * swap a b.
Used when σ = swap x y is disjoint from {a, b}: the transpositions commute, so we can rewrite
σ · (a b) as (a b) · σ. Since σ fixes both a and b, we can take z := b and τ := σ.
Proves swap a b * swap a b = 1 — a transposition is its own inverse.
Used in the cancellation case when σ = swap a b. This is the base case that terminates
iterative algorithms that repeatedly apply move_swap_left.
This lemma is a key building block for algorithms on permutations in Lean 4. It provides a constructive way to "normalize" products of transpositions by repeatedly moving a fixed element to the left. For example, given a permutation as a product τ₁ · τ₂ · ... · τₙ of transpositions, we can use move_swap_left to rewrite each τᵢ · (a b) into a form where (a ·) appears on the left, eventually factoring out all transpositions involving a. This is the foundation for algorithms computing cycle decompositions, checking permutation equivalence, and proving properties like the sign of a permutation. The exhaustive case analysis (four cases covering all possible overlaps) ensures the lemma applies to every situation, making it a robust tool for permutation reasoning.